#if !defined(__BT_H)
#define __BT_H 1

#include <stack>

// #include "mac4.h"

#ifndef MAC_HEADER_FILE
 #error You need to define MAC_HEADER_FILE in the command line of compiler
#endif
 
#include MAC_HEADER_FILE

class BT :public AC_CLASS {

  //-------------variable with permanent value----------------
  bool satisfiable;
  int numOfFailedAssignments;
  int maxSuccessfulPhase; // the longest partial assignment
  int numOfBacktracks;
  int numPruned;

#ifdef EXTENDED_STATISTICS
  int* backtrack_levels;
  int deepest_backtrack;
#endif

  //-------------data needs maintained during backtracking-----
  //valueOfVars[i] returns
  // -1: i is not assigned,
  //  p: i is assigned value p.
  // the size of the array is n.
  int *valueOfVars;
                                                                                   
  typedef struct {
    int var;
    int value;
    int phase;
  } Assignment;
  // This backups all previous assignments
  //std::stack<Assignment> preAssignments;
  int *assignedVars;  

  list<int> pruneThese;
#ifdef DOMAIN_SPLIT
  int *domainSet;
  int *maxDomSegs;
#endif

  int curVar; // the current variable
  int curValue; // the current value
  // phase is the clock which moves one step after an
  // instantiation of a variable.
  int phase; 
  //used for determination of backtracking in certain functions
  int lastPhase;

  bool hasRanked;
#ifdef VAL_COMPUTE
  double* currRankS;
  double* nextRankS;
  double* currRankC;
  double* nextRankC;
#endif

  void restoreBT(int);
  void restoreVars(int);
  void adjustDegree(int,bool);
  bool validValue(int);

  bool currSubset(list<int>&,list<int>&);
  void pruneSingle(int,int);
#ifdef VAL_COMPUTE
  void pruneSimilar(int,int);
  void pruneVariable(int,int);
#endif
  void pruneNone(int,int);

#ifdef VAL_COMPUTE
   void printCurrSupCon(int,int);
   int currSup(int,int);
   int currCon(int,int);
#endif

  //------------ disposable variables---------------------------

  //------------ internal methods ------------------------------
  
  void initBT();
  
  int lex();
  int dom();
  int deg();
  int futdeg();
  int DD();
  int DyDD();
  
  int H_1_DD_plus();
  int pagerankD();
  int pagerank3();

  void noPruneNext(int&,int&);
  void varNext(int&,int&);
  void varNextForceOld(int&,int&);
#ifdef VAL_COMPUTE
  void valuerank(int&,int&);
  void valuerank2(int&,int&);
  void valuerankVV(int&,int&);

  int VVrank(int,int);
  int VVrankQ(int,int);
#endif

  void assignVar(int, int);
  virtual bool isAssigned(int);

#ifdef DOMAIN_SPLIT
  bool nextSeg();
  bool initSplit();
  bool permMaint();
#endif
 public:
  BT(int, int, int, int, int *);
  BT(int, int);
  BT(const char *);
  virtual ~BT();
  
  bool solve();
  // return the current phase (search tree level)
  int  getPhase()
  {
    return phase;
  }


  void printSolution();
#ifdef VAL_COMPUTE
  void printValueSelection();
#endif
  void printSystem();
  void checkSolution();
  virtual void statistics();
  int getNumOfBacktracks();
  int getMaxSearchDepth();

  //int statistics();
};

#endif
